m:, n:{0..(m+1)}. upto(m) ~ (upto(n) @ map(x.x+n;upto(m - n))) 

latex

Definitions	x:A. B(x), upto(n), t  T, Y, if b then t else f fi , (i = j), tt, P  Q, i  j , A  B, A, False, as @ bs, map(f;as), SQType(T), {T}, , Top, , S  T, ff, {i..j}, i  j < k, P & Q, Dec(P), P  Q, , Unit, P  Q,
Lemmas	int sq, nat wf, int seg wf, nat properties, ge wf, decidable int equal, append nil sq, upto wf, le wf, top wf, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, append assoc sq, map wf, map append sq